
var mainUseCaseDivId = "info";
var lastDivId = 0;

function shDiv(divId) {
  var div = document.getElementById(divId);
  if(div.style.display == "none") {
    div.style.display = "block";
  } else {
    div.style.display = "none";
  }
  lastDivId = divId;
}

function shUseCase(divId) {

  shDiv(mainUseCaseDivId);
  shDiv(divId);

  mainUseCaseDivId = divId;

}


function shLastDiv()
{ 
  if(lastDivId!=0) {
    shDiv(lastDivId);
  }
}




var style = 0;
function toggleStyleSheet()
{
  if (!document.styleSheets[style].disabled) {
    document.styleSheets[style].disabled = true;
  }
  else {
    document.styleSheets[style].disabled = false;
  }

}

// XXX This is a workaround for a bug where
// changing the disabled state of a stylesheet can't
// be done in an event handler. For now, we do it
// in a zero-delay timeout.
function initiateToggle(styleno)
{
  style = styleno;
  setTimeout(toggleStyleSheet, 0);
}

